1. $T$ : Type
\\[0ex]2. $l_{1}$ : $T$ List
\\[0ex]3. $l_{2}$ : $T$ List
\\[0ex]4. $\parallel$$l_{1}$$\parallel$ $\leq$ $\parallel$$l_{2}$$\parallel$
\\[0ex]5. $\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$$l_{1}$$\parallel$) $\Rightarrow$ ($l_{1}$[$i$] = $l_{2}$[(($\parallel$$l_{2}$$\parallel$ {-} $\parallel$$l_{1}$$\parallel$)+$i$)])
\\[0ex]$\vdash$  $l_{2}$ = (firstn($\parallel$$l_{2}$$\parallel$ {-} $\parallel$$l_{1}$$\parallel$;$l_{2}$) @ $l_{1}$)